COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.cb ON THE APPLICATIONS OF SECOND ORDER LOGIC TO AI AND MTC
C00004 ENDMK
C⊗;
.cb ON THE APPLICATIONS OF SECOND ORDER LOGIC TO AI AND MTC

	The work with Corky has brought first order logic to the
limits of its applicability, and it is now worthwhile to start
collecting applications of second order logic with a view to either
translating them down, developing a second order system, or going
on to yet higher order logic.

	Among the ideas to pursue is that of the treating
finding models as just another kind of instantiation with the idea
that deciding that < on the natural numbers is an instantiation
of ∀x∃yGxy ∧ ∀x(¬Gxx) ∧ transitive G  is just an example of pattern
matching for G.  It seems reasonable to try to get rid of the
individual variables but allow variables at higher level (perhaps
I'll regret my criticism of Backus for doing just this in another
context).  The intuition is that finding an instance is always
a finite operation even when the description ostensibly involves
quantification, i.e. "take < on the integers" is a finite statement.